Nuprl Lemma : R-all-rule2 11,40

T:Type{i}, L:(T List), R:({x:T| (x  L)} es_realizer{i:l}),
P:({x:T| (x  L)} event_system{i:l}prop{i':l}).
(x,y:T. decidable((x = y)))
 l_all(LTx.R-realizes{i:l}(R(x); es.P(x,es)))
 l_all(LTx.l_all(LTy.(((x = y  T))  R-compat{i:l}(R(x); R(y)))))
 R-realizes{i:l}
 R-realizes(Rall(Lx.R(x)); es.l_all(LTx.P(x,es))) 
latex


Definitionsguard(T), P  Q, xt(x), t  T, x(s1,s2), x(s), l_all(LTx.P(x)), P  Q, prop{i:l}, x:AB(x), decidable(P)
Lemmases realizer wf, decidable wf, event system wf, R-realizes wf, R-compat wf, not wf, l member wf, R-all-rule

origin